SherbyNet - /page/wikibook/entry.mu

Micron Document

<!DOCTYPE html>

<title>Fitch notation</title>

</head>

<span id="openzim-page-title" class="mw-page-title-main"><span class="mw-page-title-main">Fitch notation</span></span>

</h1>

</header>

</p>

<p><b>Fitch notation</b>, also known as <b>Fitch diagrams</b> (named after <a href="Frederic_Fitch" title="Frederic Fitch">Frederic Fitch</a>), is a method of presenting <a href="Natural_deduction" title="Natural deduction">natural deduction</a> proofs in <a href="Propositional_calculus" class="mw-redirect" title="Propositional calculus">propositional calculus</a> and <a href="First-order_logic" title="First-order logic">first-order logics</a> using a structured, line-by-line format that explicitly shows assumptions, inferences, and their scope. It was invented by <a href="Frederic_Fitch" title="Frederic Fitch">Frederic Brenton Fitch</a> in the 1930s and later popularized through his textbook <i>Symbolic Logic</i> (1952).<sup id="cite_ref-FOOTNOTEFitch1952_1-0" class="reference"><a href="#cite_note-FOOTNOTEFitch1952-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> Fitch notation is notable for its use of indentation or boxes to indicate the scope of subordinate assumptions, making it one of the most pedagogically accessible systems for teaching formal logic.

</p>

<div class="mw-heading mw-heading2"><h2 id="History">History</h2></div>

<p>Fitch developed his system of natural deduction as part of his doctoral work at <a href="Princeton_University" title="Princeton University">Princeton University</a> in 1934, under the supervision of <a href="Alonzo_Church" title="Alonzo Church">Alonzo Church</a>. His approach introduced the key idea of <b>subordinate proofs</b>, where assumptions could be opened within a subderivation and discharged later, such as when proving implications or negations. While his system was initially circulated in unpublished form, it became widely known through his book <i>Symbolic Logic</i>,<sup id="cite_ref-FOOTNOTEFitch1952_1-1" class="reference"><a href="#cite_note-FOOTNOTEFitch1952-1"><span class="cite-bracket">[</span>1<span class="cite-bracket">]</span></a></sup> which was used extensively in undergraduate instruction.

</p><p>Later logicians and educators such as <a href="Patrick_Suppes" title="Patrick Suppes">Patrick Suppes</a><sup id="cite_ref-FOOTNOTESuppes1957_2-0" class="reference"><a href="#cite_note-FOOTNOTESuppes1957-2"><span class="cite-bracket">[</span>2<span class="cite-bracket">]</span></a></sup> and <a href="John_Lemmon" title="John Lemmon">E. J. Lemmon</a><sup id="cite_ref-FOOTNOTELemmon1965_3-0" class="reference"><a href="#cite_note-FOOTNOTELemmon1965-3"><span class="cite-bracket">[</span>3<span class="cite-bracket">]</span></a></sup> rebranded Fitch's system. While they introduced graphical changes—such as replacing indentation with vertical bars—the underlying structure of Fitch-style natural deduction remained intact. These variations are often referred to as the <a href="Suppes%E2%80%93Lemmon_notation" title="Suppes–Lemmon notation">Suppes–Lemmon format</a>, though they are fundamentally based on Fitch's original notation.

</p>

<div class="mw-heading mw-heading2"><h2 id="Structure">Structure</h2></div>

<p>Fitch notation presents proofs as a sequence of numbered lines, where each line includes:

</p>

<ul><li>A logical formula</li>

<li>A justification (a rule name and line references)</li>

<li>Optionally, indentation or brackets to show the scope of assumptions</li></ul>

<div class="mw-heading mw-heading3"><h3 id="Example">Example</h3></div>

<p>Each row in a Fitch-style proof is either:

</p>

<ul><li>an assumption or subproof assumption.</li>

<li>a sentence justified by the citation of (1) a <a href="Rule_of_inference" title="Rule of inference">rule of inference</a> and (2) the prior line or lines of the proof that license that rule.</li></ul>

<p>Introducing a new assumption increases the level of indentation, and begins a new vertical "scope" bar that continues to indent subsequent lines until the assumption is discharged. This mechanism immediately conveys which assumptions are active for any given line in the proof, without the assumptions needing to be rewritten on every line (as with sequent-style proofs).

</p><p>The following example displays the main features of Fitch notation:

</p>

<pre>0 |__ [assumption, want P if not P]

1 | |__ P [assumption, want not P]

2 | | |__ not P [assumption, for reduction]

3 | | | contradiction [contradiction introduction: 1, 2]

4 | | not not P [negation introduction: 2]

5 | |__ not not P [assumption, want P]

6 | | P [negation elimination: 5]

7 | P iff not not P [biconditional introduction: 1 - 4, 5 - 6]

</pre>

<li>The null assumption, <i>i.e.</i>, we are proving a <a href="Tautology_(logic)" title="Tautology (logic)">tautology</a></li>

<li>Our first subproof: we assume the l.h.s. to show the r.h.s. follows</li>

<li>A subsubproof: we are free to assume what we want. Here we aim for a <a href="Reductio_ad_absurdum" title="Reductio ad absurdum">reductio ad absurdum</a></li>

<li>We now have a contradiction</li>

<li>We are allowed to prefix the statement that "caused" the contradiction with a not</li>

<li>Our second subproof: we assume the r.h.s. to show the l.h.s. follows</li>

<li>We invoke the rule that allows us to remove an even number of nots from a statement prefix</li>

<li>From 1 to 4 we have shown if P then not not P, from 5 to 6 we have shown P if not not P; hence we are allowed to introduce the biconditional in 7, where <i>iff</i> stands for <i>if and only if</i></li>

</ol>

<div class="mw-heading mw-heading2"><h2 id="Features">Features</h2></div>

<ul><li><b>Subordinate proofs</b>: Nested derivations with temporarily assumed premises</li>

<li><b>Assumption discharge</b>: Explicit rules like <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \to }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \to }</annotation>

</semantics>

</math></span><img src="./1daab843254cfcb23a643070cf93f3badc4fbbbd.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: -0.338ex; width:2.324ex; height:1.843ex;" alt="{\displaystyle \to }" loading="lazy"></span> introduction and <span class="mwe-math-element mwe-math-element-inline"><span class="mwe-math-mathml-inline mwe-math-mathml-a11y" style="display: none;"><math xmlns="http://www.w3.org/1998/Math/MathML" alttext="{\displaystyle \neg }">

</mstyle>

</mrow>

<annotation encoding="application/x-tex">{\displaystyle \neg }</annotation>

</semantics>

</math></span><img src="./fa78fd02085d39aa58c9e47a6d4033ce41e02fad.svg" class="mwe-math-fallback-image-inline mw-invert skin-invert" aria-hidden="true" style="vertical-align: 0.204ex; margin-bottom: -0.376ex; width:1.55ex; height:1.176ex;" alt="{\displaystyle \neg }" loading="lazy"></span> introduction for closing assumptions</li>

<li><b>Line-referenced justification</b>: Each step cites lines and rules used</li>

<li><b>Human readability</b>: The format closely mirrors natural informal reasoning</li></ul>

<div class="mw-heading mw-heading2"><h2 id="Comparison_with_Other_Systems">Comparison with Other Systems</h2></div>

<ul><li><a href="Natural_deduction#Gentzen's_tree_notation" title="Natural deduction">Gentzen-style natural deduction</a> presents proofs as trees, with assumptions at the leaves and conclusions at the root. Unlike Fitch notation, it does not use subordinate boxes or indentation to manage temporary assumptions. Instead, all assumptions are explicitly present in the leaf nodes of the proof tree. This uniform treatment of assumptions makes Gentzen systems particularly well-suited to structural proof transformations and facilitates modularization and meta-theoretical analysis, such as cut-elimination.</li>

<li><a href="Hilbert_system" title="Hilbert system">Hilbert system</a> proofs rely on axioms and only a few inference rules, making them concise but abstract and less intuitive.</li>

<li>The <a href="Suppes%E2%80%93Lemmon_notation" title="Suppes–Lemmon notation">Suppes–Lemmon notation</a> follows Fitch's logic and alters its visual layout for typesetting and instructional clarity.</li></ul>

<div class="mw-heading mw-heading2"><h2 id="Influence">Influence</h2></div>

<p>Fitch notation is widely used in <a href="Logic" title="Logic">logic</a> textbooks and teaching. It also underlies several <a href="Proof_assistant" title="Proof assistant">proof assistant</a> tools. Its structured style has become a standard for teaching formal logic in undergraduate education.

</p>

<ul><li><a href="Natural_deduction" title="Natural deduction">Natural deduction</a></li>

<li><a href="Frederic_Fitch" title="Frederic Fitch">Frederic Fitch</a></li>

<li><a href="Sequent_calculus" title="Sequent calculus">Sequent calculus</a></li>

<li><a href="Proof_theory" title="Proof theory">Proof theory</a></li>

<li><a href="Hilbert_system" title="Hilbert system">Hilbert system</a></li>

<li><a href="Suppes%E2%80%93Lemmon_notation" title="Suppes–Lemmon notation">Suppes–Lemmon notation</a></li></ul>

<div class="mw-heading mw-heading2"><h2 id="Notes">Notes</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output .reflist{margin-bottom:0.5em;list-style-type:decimal}@media screen{.mw-parser-output .reflist{font-size:90%}}.mw-parser-output .reflist .references{font-size:100%;margin-bottom:0;list-style-type:inherit}.mw-parser-output .reflist-columns-2{column-width:30em}.mw-parser-output .reflist-columns-3{column-width:25em}.mw-parser-output .reflist-columns{margin-top:0.3em}.mw-parser-output .reflist-columns ol{margin-top:0}.mw-parser-output .reflist-columns li{page-break-inside:avoid;break-inside:avoid-column}.mw-parser-output .reflist-upper-alpha{list-style-type:upper-alpha}.mw-parser-output .reflist-upper-roman{list-style-type:upper-roman}.mw-parser-output .reflist-lower-alpha{list-style-type:lower-alpha}.mw-parser-output .reflist-lower-greek{list-style-type:lower-greek}.mw-parser-output .reflist-lower-roman{list-style-type:lower-roman}

/* end https://en.wikipedia.org/ */

</style><div class="reflist">

<li id="cite_note-FOOTNOTEFitch1952-1"><span class="mw-cite-backlink">^ <a href="#cite_ref-FOOTNOTEFitch1952_1-0"><sup><i><b>a</b></i></sup></a> <a href="#cite_ref-FOOTNOTEFitch1952_1-1"><sup><i><b>b</b></i></sup></a></span> <span class="reference-text"><a href="#CITEREFFitch1952">Fitch 1952</a>.</span>

</li>

<li id="cite_note-FOOTNOTESuppes1957-2"><span class="mw-cite-backlink"><b><a href="#cite_ref-FOOTNOTESuppes1957_2-0">^</a></b></span> <span class="reference-text"><a href="#CITEREFSuppes1957">Suppes 1957</a>.</span>

</li>

<li id="cite_note-FOOTNOTELemmon1965-3"><span class="mw-cite-backlink"><b><a href="#cite_ref-FOOTNOTELemmon1965_3-0">^</a></b></span> <span class="reference-text"><a href="#CITEREFLemmon1965">Lemmon 1965</a>.</span>

</li>

</ol></div></div>

<div class="mw-heading mw-heading2"><h2 id="References">References</h2></div>

/* start https://en.wikipedia.org/ */

.mw-parser-output cite.citation{font-style:inherit;word-wrap:break-word}.mw-parser-output .citation q{quotes:"\"""\"""'""'"}.mw-parser-output .citation:target{background-color:rgba(0,127,255,0.133)}.mw-parser-output .id-lock-free.id-lock-free a{background:url("./mw/Lock-green.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-limited.id-lock-limited a,.mw-parser-output .id-lock-registration.id-lock-registration a{background:url("./mw/Lock-gray-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .id-lock-subscription.id-lock-subscription a{background:url("./mw/Lock-red-alt-2.svg")right 0.1em center/9px no-repeat}.mw-parser-output .cs1-ws-icon a{background:url("./mw/Wikisource-logo.svg")right 0.1em center/12px no-repeat}body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-free a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-limited a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-registration a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .id-lock-subscription a,body:not(.skin-timeless):not(.skin-minerva) .mw-parser-output .cs1-ws-icon a{background-size:contain;padding:0 1em 0 0}.mw-parser-output .cs1-code{color:inherit;background:inherit;border:none;padding:inherit}.mw-parser-output .cs1-hidden-error{display:none;color:var(--color-error,#d33)}.mw-parser-output .cs1-visible-error{color:var(--color-error,#d33)}.mw-parser-output .cs1-maint{display:none;color:#085;margin-left:0.3em}.mw-parser-output .cs1-kern-left{padding-left:0.2em}.mw-parser-output .cs1-kern-right{padding-right:0.2em}.mw-parser-output .citation .mw-selflink{font-weight:inherit}@media screen{.mw-parser-output .cs1-format{font-size:95%}html.skin-theme-clientpref-night .mw-parser-output .cs1-maint{color:#18911f}}@media screen and (prefers-color-scheme:dark){html.skin-theme-clientpref-os .mw-parser-output .cs1-maint{color:#18911f}}

/* end https://en.wikipedia.org/ */

</style><cite id="CITEREFFitch1952" class="citation book cs1"><a href="Frederic_Fitch" title="Frederic Fitch">Fitch, Frederic Brenton</a> (1952). <i>Symbolic Logic: An introduction</i>. New York: The Ronald Press Company. <a href="LCCN_(identifier)" class="mw-redirect" title="LCCN (identifier)">LCCN</a> <a rel="nofollow" class="external text" href="https://lccn.loc.gov/52006196">52006196</a>.</cite></li></ul>

<ul><li><cite id="CITEREFBarker-PlummerBarwiseEtchemendy2011" class="citation book cs1">Barker-Plummer, Dave; <a href="Jon_Barwise" title="Jon Barwise">Barwise, Jon</a>; <a href="John_Etchemendy" title="John Etchemendy">Etchemendy, John</a> (2011) [1999]. <i><a href="Language%2C_Proof_and_Logic" title="Language, Proof and Logic">Language, Proof and Logic</a></i> (2 ed.). CSLI Publications. p. 606. <a href="ISBN_(identifier)" class="mw-redirect" title="ISBN (identifier)">ISBN</a> <bdi>9781575866321</bdi>.</cite></li>

<li><cite id="CITEREFLemmon1965" class="citation book cs1"><a href="John_Lemmon" title="John Lemmon">Lemmon, E. J.</a> (1965). <i>Beginning Logic</i>. Nelson.</cite></li>

<li><cite id="CITEREFSuppes1957" class="citation book cs1"><a href="Patrick_Suppes" title="Patrick Suppes">Suppes, Patrick</a> (1957). <i>Introduction to Logic</i>. Van Nostrand.</cite></li></ul>

<div class="mw-heading mw-heading2"><h2 id="External_links">External links</h2></div>

<ul><li><cite id="CITEREFBrogaardSalerno2019" class="citation encyclopaedia cs1"><a href="Berit_Brogaard" title="Berit Brogaard">Brogaard, Berit</a>; Salerno, Joe (Fall 2019). <a rel="nofollow" class="external text" href="https://plato.stanford.edu/entries/fitch-paradox/">"Fitch's Paradox of Knowability"</a>. In <a href="Edward_N._Zalta" title="Edward N. Zalta">Zalta, Edward N.</a> (ed.). <i><a href="Stanford_Encyclopedia_of_Philosophy" title="Stanford Encyclopedia of Philosophy">Stanford Encyclopedia of Philosophy</a></i>.</cite></li>

<li><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://web.archive.org/web/20061002151420/http://logik.phl.univie.ac.at/%7Echris/gateway/formular-uk-fitch.html">"An online Java application for proof building"</a>. Archived from <a rel="nofollow" class="external text" href="http://logik.phl.univie.ac.at/~chris/gateway/formular-uk-fitch.html">the original</a> on 2 October 2006<span class="reference-accessdate">. Retrieved <span class="nowrap">6 May</span> 2025</span>.</cite></li>

<li><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://proofmood.mindconnect.cc/">"A Web implementation of Fitch proof system (propositional and first-order)"</a>. <i>proofmod.mindconnect.cc</i><span class="reference-accessdate">. Retrieved <span class="nowrap">6 May</span> 2025</span>.</cite></li>

<li><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://github.com/RBornat/jape/">"The Jape general-purpose proof assistant"</a>. <i>GitHub</i><span class="reference-accessdate">. Retrieved <span class="nowrap">6 May</span> 2025</span>.</cite> (see <a href="Jape_(software)" title="Jape (software)">Jape</a>)</li>

<li><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://www.logicmatters.net/latex-for-logicians/nd/">"Resources for typesetting proofs in Fitch notation with LaTeX"</a>. <i>Logic Matters</i><span class="reference-accessdate">. Retrieved <span class="nowrap">6 May</span> 2025</span>.</cite> (see <a href="LaTeX" title="LaTeX">LaTeX</a>)</li>

<li><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://mrieppel.github.io/fitchjs/">"FitchJS: An open source web app to construct proofs in Fitch notation (and export to LaTeX)"</a><span class="reference-accessdate">. Retrieved <span class="nowrap">6 May</span> 2025</span>.</cite></li>

<li><cite class="citation web cs1"><a rel="nofollow" class="external text" href="https://proofs.openlogicproject.org/">"Natural deduction proof editor and checker in Fitch notation"</a><span class="reference-accessdate">. Retrieved <span class="nowrap">6 May</span> 2025</span>.</cite></li></ul></div><div><div class="zim-footer">

This article is issued from <a class="external text" title="Last edited on 2025-05-06" href="https://en.wikipedia.org/wiki/?title=Fitch_notation&oldid=1289100867">Wikipedia</a>. The text is available under <a class="external text" href="https://creativecommons.org/licenses/by-sa/4.0/deed.en">Creative Commons Attribution-Share Alike 4.0</a> unless otherwise noted. Additional terms may apply for the media files.

</div>

</div></div>

</div>

</main>

</div>

</body></html>